Nuprl Lemma : no_repeats_member
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
x
:
T
. no_repeats(
T
;
L
)
(
x
L
)
l_member!(
x
;
L
;
T
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
no_repeats(
T
;
l
)
,
(
x
l
)
,
l_member!(
x
;
l
;
T
)
,
P
Q
,
False
,
A
,
A
B
,
,
A
c
B
,
x
:
A
.
B
(
x
)
,
P
Q
,
prop{i:l}
,
guard(
T
)
,
P
Q
,
P
Q
,
P
Q
Lemmas
cons
member
,
cons
member!
,
no
repeats
cons
,
l
member!
wf
,
not
wf
,
l
member
wf
,
no
repeats
wf
origin
T:Type, L:(T List), x:T. no_repeats(T; L) 
(x 
L) l_member!(x; L; T) T:Type, L:(T List), x:T. no_repeats(T; L) (x L) l_member!(x; L; T) Tx:A. B(x) l) Q
A
B
B
x:A. B(x) Q
Q
Q Q